Highly-integrated complex system-on-chip (SoC) devices power a wide range of systems, ranging from mobile computing devices to automotive control systems. One factor aiding the advancement and proliferation of these complex devices includes the use of readily available reusable semiconductor intellectual property (IP). Reusable semiconductor IP provides designers with a variety of silicon proven subsystem blocks, including processors, memory controllers, physical interfaces (PHYs), and input/output (I/O) circuits. But the integration of reusable semiconductor IP also adds to the growing challenges facing design verification engineers.
Multisystem SoCs present complex system issues that can be difficult and time consuming to identify and solve, even for experienced design verification engineers. These issues include verifying that multiple subsystems operate as a system and stressing subsystem interfaces to fully characterize and verify transaction flow between subsystem modules. While verification tools have improved, current verification methods still require significant expertise and experience to quickly identify and debug complex interface and interconnect problems. In many cases, verification tools lack the capability to interact with verification engineers in a manner to leverage their expertise to address this complexity. The presence of deadlocks where an electronic design remains at a particular state for an extended period of time presents further challenges to verification tools.
Conventional deadlock detection approaches using formal verification techniques are typically done with liveness assertions that check whether the design will transition out of a particular state. For example, a liveness assertion might be written to check that whenever a state machine is on state BUSY, it will eventually transition out of BUSY in the future. Liveness assertions will either follow LTL or CTL semantics. LTL liveness assertions will check that the design always transitions to a certain state. CTL liveness assertions will check that the design can always transition to a certain state. This difference is important because it impacts how the environment has to be constrained in order to catch real deadlock issues.
Some conventional approaches use simulations to detect deadlocks. Given a certain stimulus, the simulation testbench checks whether the design is back to an idle state at the end of the simulation. If it is not, then the design deadlocked along the test. Because the stimulus is provided by the user, micro-architectural analysis usually takes place before investing in the simulation testbench, to try to predict where and how deadlocks may happen, so the stimulus can focus on these areas.
Furthermore, the analysis of liveness assertions by modern model checkers is a computationally-intensive task and does not scale well with design sizes nowadays. Hence, this conventional approach is often limited to small electronic designs. When using LTL liveness assertions—the most common approach—another issue is that they require fairness constraints in order to avoid false negatives. The fairness constraints guarantee that design inputs will have the necessary activity which will prevent the design from deadlocking. For example, to prove that a state machine always eventually transitions out of state BUSY, it might be required to add a fairness constraint saying that that state machine will eventually get a response from another block.
Specification and/or verification of CTL liveness assertions may not be supported by most model checkers. In some cases where model checkers support specification and/or verification of CTL liveness assertions, one of the main challenges is then the fact that the semantics of CTL assertions are very hard to explain to users without extensive formal verification background, and thus making it unusable to most. Finally, bugs caught by CTL liveness assertions have to show that there is a case where the design cannot return to a certain state, which usually cannot be easily captured in a waveform. When using simulation techniques, the effectiveness of simulation depends on how the user set up the stimulus. In particular with deadlock detection, trying to predict areas where deadlocks may occur may be extremely challenging and error prone, as often these issues occur where it was not expected. Moreover, it has been observed that the stimulus that causes a deadlock may have very strict timing requirements, rendering it hard for users to reproduce a deadlock in simulation even when the area where it occurs is known a priori.
Thus, what are needed are methods, systems, and computer program products for deadlock verification of electronic designs using formal techniques to improve deadlock detection while reducing computational intensity and to address at least the aforementioned issues and shortcomings.